Z3是由Microsoft Research开发的高性能定理证明器。接下来将使用Python3中的Z3库来实现对数独问题的解决。 关于Python中Z3的使用入门，可以参考这篇博文https://blog.csdn.net/yalecaltech/article/details/90575076

数独问题就是在一个 9 × 9 9\times 9 9×9的格网的每个格子中填入0~9九个数字之一，使得每一行、每一列、每一宫（将整个盘面均分为9个 3 × 3 3\times 3 3×3的九宫格，即为九个宫）中的数都不重复。记 A i j A_{ij} Aij​为第 i i i行第 j j j列的数，本问题的约束条件就是 ∀ i ∀ j ∀ k ( i ≠ k ∧ j ≠ k → ( A i j ≠ A i k ) ∧ ( A i j ≠ A k j ) ) \forall i\forall j\forall k(i\neq k\land j\neq k\rightarrow(A_{ij}\neq A_{ik})\land(A_{ij}\neq A_{kj})) ∀i∀j∀k(i​=k∧j​=k→(Aij​​=Aik​)∧(Aij​​=Akj​)) ∀ i ∀ j ∀ m ∀ n ( ( ( 1 ≤ i , m ≤ 3 ) ∨ ( 4 ≤ i , m ≤ 6 ) ∨ ( 7 ≤ i , m ≤ 9 ) ) ∧ ( ( 1 ≤ j , n ≤ 3 ) ∨ ( 4 ≤ j , n ≤ 6 ) ∨ ( 7 ≤ j , n ≤ 9 ) ) ∧ ( i ≠ m ∨ j ≠ n ) → ( A i j ≠ A m n ) ) \forall i\forall j \forall m\forall n(((1\le i,m\le 3)\lor(4\le i,m\le 6)\lor(7\le i,m\le9))\land ((1\le j,n\le 3)\lor(4\le j,n\le 6)\lor(7\le j,n\le9))\land(i\neq m\lor j\neq n)\rightarrow(A_{ij}\neq A_{mn})) ∀i∀j∀m∀n(((1≤i,m≤3)∨(4≤i,m≤6)∨(7≤i,m≤9))∧((1≤j,n≤3)∨(4≤j,n≤6)∨(7≤j,n≤9))∧(i​=m∨j​=n)→(Aij​​=Amn​))

最初格子内的提示数因不能更改也应该作为约束条件加入求解器中。

完整代码如下：